\section{Monotonic Framework}

Задача $SRD$. Модифицированная семантика большого шага. Неразрешимость $SRD$. 
$SUEU$ через семантику с продолжениями. Неразрешимость $SUEU$.

Сверхаппроксимация $SRD$ для линейных программ. Линейное приближение:

Пусть $P$~--- программа. \emph{Линейное приближение}~--- это не более чем счетное
множество линейных программ $\la{P}$ такое, что для любого входа
найдется такая $P_L\in\la{P}$, которая на этом входе ведет себя так же, как $P$
(возможно, потребуются некоторые модификации).

Как посчитать линейную аппроксимацию:

$$
\begin{array}{rcl}
  \la{\llang{skip}}&=&\{\llang{skip}\} \\
  \la{\llang{write ($e$)}}&=&\{\llang{write ($e$)}\}\\
  \la{\llang{read ($x$)}}&=&\{\llang{read ($x$)}\}\\
  \la{\llang{$x$ := $e$}}&=&\{\llang{$x$ := $e$}\}\\
  \la{\llang{$S_1$; $\;S_2$}}&=&\la{S_1}\times\la{S_2}\\
  \la{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}&=&\la{S_1}\cup\la{S_2}\\
  \la{\llang{while $\;e\;$ do $\;S$}}&=&fix(\lam{F}{\{\llang{skip}\}\cup\la{S}\times F})  
\end{array}
$$

\noindent где операция ``$\times$'' определена следующим образом:

$$
A\times B = \{\llang{$S_A$; $\;S_B$}\mid S_A\in A,\; S_B\in B\}
$$

``MOP''-решение (на примере $RD$): пусть $P$~--- программа, $S$~--- её оператор. Тогда:

$$
RD^{P}_{MOP}\:(S)=\bigcup_{\overline{P}\in\la{P}}RD^{\overline{P}}\:(S)
$$
